<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofUnifier</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofUnifier";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofUnifier.html" target="_top">Frames</a></li>
<li><a href="ProofUnifier.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.pa</div>
<h2 title="Class ProofUnifier" class="title">Class ProofUnifier</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.pa.ProofUnifier</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ProofUnifier</span>
extends java.lang.Object</pre>
<div class="block">ProofUnifier is a separate class simply to break out the unification code
 from everything else. Logically it could be part of ProofAsst.
 <p>
 The job here is to unify the steps in a ProofWorksheet and build the proof
 trees for the derivation steps in the proof. The proof tree of the 'qed' step
 equals the proof of the Theorem, fyi.
 <p>
 There are five main things happening here (whew!):
 <ol>
 <li>Figure out the correct sequence of the LogHyp's on each derivation step
 (if the input sequence turns out to be wrong.)
 <li>Figure out the Ref label, if not input, that justifies each derivation
 step;
 <li>Derive the step's formula and/or logical hypotheses when the Ref label is
 input and formula is missing or 0-n of the hyps are missing -- or both. This
 is the (new) Proof Assistant "Derive" Feature. An in-depth description of its
 required behaviors in ProofUnifier.java is provided below, but basically,
 once the required fields are successfully derived, the derivation step is to
 be handled normally -- and if the input Ref does not unify with its
 associated input hyp(s), then the search for alternates is performed (the
 "Derive" feature is to be tightly and seamlessly integrated into the normal
 unification process!)
 <li>When Ref label is input on a derivation step, use it instead of searching
 for it, but if the Ref label has a unification error or a Distinct Variables
 Restriction (DjVars) error, perform the search to generate a message
 informing the user of alternate Refs. In the case of a DjVars error, if
 another Ref is found that unifies perfectly without a DjVars error, take it
 (this might be slightly odd and unusual if another Ref unifies perfectly with
 "Derive" generated Hyps!)
 <li>Once a derivation step has been "unified", its proof tree must be built
 and checked for Distinct Variables Restriction errors. Since a step's proof
 tree requires that its logical hypotheses have proof trees, a derivation step
 is not errored if one of its hypotheses is not yet proved (for example, has
 "?" in its Hyp). This allows for proving backwards, from conclusion to
 premisses.
 </ol>
 <p>
 The algorithm to do these things is not godlike :) It searches for the first
 Assrt that successfully unifies with each proof step -- if the Ref is not
 input. But there may be multiple assertions that unify with a step, and it is
 possible that unification as a whole fails because an earlier step's Ref
 label is wrong. The "unification" process means finding a consistent set of
 variable substitutions. To unify an entire proof the requirement is that the
 substitutions be consistent across the entire proof. However, the algorithm
 does work for set.mm and ql.mm without any false positives. (As a fallback,
 the user can input Ref to avoid the problem of multiple possible
 unifications.)
 <p>
 Also, a RunParm is provided to specify double-checking each unification using
 the VerifyProofs.java object -- i.e. the Metamath
 "Proof Verification Engine". The default option is NO, but should probably be
 YES in practice given that response time is not a problem (yet?) This will
 catch false unifications early.
 <p>
 It should also be noted that ProofUnifier does check Distinct Variable ($d)
 restrictions as it works on each proof step. This feature is an enhancement
 to the Metamath Proof Assistant, which does not check $d's. By checking $d's
 here we also avoid false unification positives and improve the results of the
 algorithm.
 <p></div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofUnifier.html#ProofUnifier(mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.verify.VerifyProofs)">ProofUnifier</a></strong>(<a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
            <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
            <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
            <a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify">VerifyProofs</a>&nbsp;verifyProofs)</code>
<div class="block">Standard constructor for set up.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#getSortedAssrtSearchList()">getSortedAssrtSearchList</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#getTablesInitialized()">getTablesInitialized</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#getUnifySearchListByMObjSeq()">getUnifySearchListByMObjSeq</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#initializeLookupTables(mmj.lang.Messages)">initializeLookupTables</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Initialize lookup tables to be used across multiple executions of the
 GUI.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#mergeListOfAssrtAddsSortedBySeq(java.util.List)">mergeListOfAssrtAddsSortedBySeq</a></strong>(java.util.List&lt;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&gt;&nbsp;listOfAssrtAddsSortedBySeq)</code>
<div class="block">Merges a list of added Assrt objects sorted by MObj seq into the
 unifySearchList and passes the list on to the StepSelectorSearch for its
 updates.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#separateMandAndOptFrame(mmj.pa.ProofWorksheet, mmj.pa.DerivationStep, java.util.List, java.util.List, boolean)">separateMandAndOptFrame</a></strong>(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet,
                       <a href="../../mmj/pa/DerivationStep.html" title="class in mmj.pa">DerivationStep</a>&nbsp;qedStep,
                       java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;mandHypList,
                       java.util.List&lt;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;optionalVarHypList,
                       boolean&nbsp;addLogHyps)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofUnifier.html#unifyAllProofDerivationSteps(mmj.pa.ProofWorksheet, mmj.lang.Messages, boolean)">unifyAllProofDerivationSteps</a></strong>(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet,
                            <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                            boolean&nbsp;noConvertWV)</code>
<div class="block">Unifies the proof steps in a Proof Worksheet.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofUnifier(mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.verify.VerifyProofs)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofUnifier</h4>
<pre>public&nbsp;ProofUnifier(<a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
            <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
            <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
            <a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify">VerifyProofs</a>&nbsp;verifyProofs)</pre>
<div class="block">Standard constructor for set up.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>logicalSystem</code> - the loaded Metamath data</dd><dd><code>grammar</code> - the mmj.verify.Grammar object</dd><dd><code>verifyProofs</code> - the mmj.verify.VerifyProofs object</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="getUnifySearchListByMObjSeq()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getUnifySearchListByMObjSeq</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;getUnifySearchListByMObjSeq()</pre>
</li>
</ul>
<a name="getTablesInitialized()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTablesInitialized</h4>
<pre>public&nbsp;boolean&nbsp;getTablesInitialized()</pre>
</li>
</ul>
<a name="initializeLookupTables(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>initializeLookupTables</h4>
<pre>public&nbsp;boolean&nbsp;initializeLookupTables(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</pre>
<div class="block">Initialize lookup tables to be used across multiple executions of the
 GUI.
 <p>
 This is the place to create optimizations of search tables, etc. for the
 Unification process.
 <p>
 <ol>
 <li>The Grammar's Provable Logic Statement Type Code is fetched and
 cached</li>
 <li>LogicalSystem.stmtTbl is sorted into ascending database sequence
 (MObj.seq) in an ArrayList (only Theorems and Axioms with the Provable
 Logic Statment Type (i.e. "|-" are included.)</li>
 </ol></div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd>
<dt><span class="strong">Returns:</span></dt><dd>boolean true if tables initialized successfully.</dd></dl>
</li>
</ul>
<a name="getSortedAssrtSearchList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSortedAssrtSearchList</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;getSortedAssrtSearchList()</pre>
</li>
</ul>
<a name="mergeListOfAssrtAddsSortedBySeq(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>mergeListOfAssrtAddsSortedBySeq</h4>
<pre>public&nbsp;void&nbsp;mergeListOfAssrtAddsSortedBySeq(java.util.List&lt;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&gt;&nbsp;listOfAssrtAddsSortedBySeq)</pre>
<div class="block">Merges a list of added Assrt objects sorted by MObj seq into the
 unifySearchList and passes the list on to the StepSelectorSearch for its
 updates.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>listOfAssrtAddsSortedBySeq</code> - List of Assrt sorted by MObj.seq
            representing new assertions which were added to the
            LogicalSystem.</dd></dl>
</li>
</ul>
<a name="unifyAllProofDerivationSteps(mmj.pa.ProofWorksheet, mmj.lang.Messages, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unifyAllProofDerivationSteps</h4>
<pre>public&nbsp;void&nbsp;unifyAllProofDerivationSteps(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet,
                                <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                                boolean&nbsp;noConvertWV)
                                  throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Unifies the proof steps in a Proof Worksheet.
 <p>
 This is called by ProofAsst.java.
 <p>
 The "parallelStepUnificationMethod()" is used for unification. This means
 that one pass is made through LogicalSystem.stmtTbl and for each Stmt, an
 attempt is made to unify each un-unified proof step with that Stmt.
 Speed-wise, this works fine now. In theory, if set.mm had 1 million
 Theorems things would be uglier and it might be better to use Stmt lookup
 tables to unify each proof step, one by one. But today the extra coding
 effort to build those tables might not even produce an improvement in
 performance. The longest Theorem proof unification is around 500,000,000
 nanoseconds -- or 1/2 second -- which is acceptable for the
 ProofAsstGUI's response time. (The average unification time is much less,
 like 1/10 second.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofWorksheet</code> - proof in progress</dd><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd><dd><code>noConvertWV</code> - true if we should not replace work vars with dummy
            vars in derivation steps</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if unification was unsucessful</dd></dl>
</li>
</ul>
<a name="separateMandAndOptFrame(mmj.pa.ProofWorksheet, mmj.pa.DerivationStep, java.util.List, java.util.List, boolean)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>separateMandAndOptFrame</h4>
<pre>public static&nbsp;void&nbsp;separateMandAndOptFrame(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet,
                           <a href="../../mmj/pa/DerivationStep.html" title="class in mmj.pa">DerivationStep</a>&nbsp;qedStep,
                           java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;mandHypList,
                           java.util.List&lt;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;optionalVarHypList,
                           boolean&nbsp;addLogHyps)</pre>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofStepStmt.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofUnifier.html" target="_top">Frames</a></li>
<li><a href="ProofUnifier.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
